/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BAXB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30



␈↓ ↓H␈↓α␈↓ ∧UA NATURAL REPRESENTATION

␈↓ ↓H␈↓␈↓ α_Here␈α⊂is␈α⊂a␈α⊂systematic␈α⊂way␈α⊃of␈α⊂representing␈α⊂recursively␈α⊂defined␈α⊂functions␈α⊃by␈α⊂non-recursive
␈↓ ↓H␈↓sentences of first order logic.  Suppose the function is given by

␈↓ ↓H␈↓1)␈↓ α8  ␈↓↓f = Y(F)␈↓

␈↓ ↓H␈↓in Scottish.  We define

␈↓ ↓H␈↓2)␈↓ α8  ␈↓↓ x εε w ≡ ∃w1.(w1 subexp w ∧ x = ␈↓αaa␈↓↓ w1)␈↓,

␈↓ ↓H␈↓and

␈↓ ↓H␈↓3)␈↓ α8  ␈↓↓α(w,x) = ␈↓αif␈↓↓ ␈↓αn␈↓↓ assoc(x,w) ␈↓αthen␈↓↓ ␈↓	W␈↓↓ ␈↓αelse␈↓↓ ␈↓αd␈↓↓ assoc(x,w)␈↓.

␈↓ ↓H␈↓We then define

␈↓ ↓H␈↓4)␈↓ α8  ␈↓↓∀w.[compseq(w,F) ≡ ∀x.[x εε w ≡ α(w,x) = F(λz.α(w,z))(x)]]␈↓

␈↓ ↓H␈↓from which follows

␈↓ ↓H␈↓5)␈↓ α8  ␈↓↓∀x y.[y = f(x) ≡ ∃w.[compseq(w,F) ∧ y = α(w,x)]]␈↓.

␈↓ ↓H␈↓␈↓ α_The␈αfunctions␈αε,␈αεε␈αand␈αα␈αare␈α
all␈αrepresentable␈αusing␈α␈↓↓subexp␈↓.␈α Sentences␈α(4)␈αand␈α(5)␈α
are␈αnot
␈↓ ↓H␈↓first␈α∂order␈α∂in␈α∂␈↓↓F,␈↓␈α∂but␈α∂for␈α∂any␈α⊂fixed␈α∂␈↓↓F␈↓␈α∂they␈α∂become␈α∂first␈α∂order␈α∂sentences.␈α∂ Consider␈α⊂the␈α∂rather
␈↓ ↓H␈↓complicated recursive definition

␈↓ ↓H␈↓6)␈↓ α8  ␈↓↓f x ← ␈↓αif␈↓↓ p1 x ␈↓αthen␈↓↓ g1 x ␈↓αelse␈↓↓ ␈↓αif␈↓↓ p2(x,f h1 x) ␈↓αthen␈↓↓ g2 x ␈↓αelse␈↓↓ g3(x,f g4(x,f g5 x))␈↓.

␈↓ ↓H␈↓(4) and (5) then give

␈↓ ↓H␈↓7)␈↓ α8  ␈↓↓∀x y.[y = f x ≡ ∃w.[y = α(w,x) ∧ ∀x.[x εε w ≡
␈↓ ↓H␈↓↓α(w,x) = ␈↓αif␈↓↓ p1 x ␈↓αthen␈↓↓ g1 x ␈↓αelse␈↓↓ ␈↓αif␈↓↓ p2(x,α(w,h1 x)) ␈↓αthen␈↓↓ g2 x ␈↓αelse␈↓↓ g3(x,α(w,g4(x,α(w,g5 x))))]]]␈↓.

␈↓ ↓H␈↓Our␈αobject␈αin␈α
devising␈αthe␈αnotation␈αwas␈α
to␈αmake␈αa␈αparallel␈α
between␈αthe␈αrecursive␈α
definition␈αand
␈↓ ↓H␈↓the␈αrepresenting␈αformula.␈α The␈αparallel␈αwould␈αbe␈αeven␈αmore␈αstriking␈αif␈αwe␈αsugared␈αthe␈αsyntax␈αby
␈↓ ↓H␈↓writing␈α
(say)␈α
␈↓↓f'␈↓␈α
instead␈α∞of␈α
␈↓↓w␈↓␈α
and␈α
writing␈α∞␈↓↓f'␈↓π<␈↓↓x␈↓π>␈↓␈α
instead␈α
of␈α
␈↓↓α(f',x)␈↓.␈α
 In␈α∞any␈α
case,␈α
we␈α
can␈α∞use␈α
the
␈↓ ↓H␈↓algebraic structure of the recursive definition in reasoning that uses the representation formula.